<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>



<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<META name="GENERATOR" content="hevea 1.08">
<LINK rel="stylesheet" type="text/css" href="libman.css">
<TITLE>
Invoking and Using Propia
</TITLE>
</HEAD>
<BODY >
<A HREF="libman039.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="libman038.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="libman041.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
<HR>

<H2 CLASS="section"><A NAME="htoc77">7.2</A>&nbsp;&nbsp;Invoking and Using Propia</H2>
Propia is an ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP>library, loaded by calling
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
?- lib(propia).
</PRE></BLOCKQUOTE>
A goal, such as <CODE>member(X,[1,2,3])</CODE>, is turned into a constraint
by annotating it using the <CODE>infers</CODE> operator.
The second argument of <CODE>infers</CODE> defines how much propagation
should be attempted on the constraint and will be described in
section <A HREF="libman041.html#approx">7.3</A> below. 
In this section we shall use <CODE>Goal infers most</CODE>, which infers as
much information as possible, given the loaded constraint solvers. If
the <CODE>IC</CODE> solver is loaded, then <CODE>IC</CODE> information is
extracted, and Propia reduces the domains to achieve arc-consistency.<BR>
<BR>
We first show the behaviour of the original goal:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
?- member(X, [1, 2, 3]).
X = 1
Yes (0.00s cpu, solution 1, maybe more)
X = 2
Yes (0.02s cpu, solution 2, maybe more)
X = 3
Yes (0.02s cpu, solution 3)
</PRE></BLOCKQUOTE>
<A NAME="@default204"></A>
Constraint propagation is invoked by <CODE>infers most</CODE>:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
?- lib(ic).
...
?- member(X, [1, 2, 3]) infers most.
X = X{1 .. 3}
Yes (0.00s cpu)
</PRE></BLOCKQUOTE>
Note that the information produced by the constraint solves the
corresponding goal as well.
The constraint can thus be dropped.<BR>
<BR>
In case there remains information not yet extracted, the constraint
must delay so that completeness is preserved:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
?- member(X,Y) infers most.

X = X
Y = [H3|T3]
Delayed goals:
    member(X, [H3|T3]) infers most
yes.
</PRE></BLOCKQUOTE>
Propia copes correctly with built-in predicates, such as #&gt;and
#&lt;, so after compiling this simple program:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
notin3to6(X) :- X#&lt;3.
notin3to6(X) :- X#&gt;6.
</PRE></BLOCKQUOTE>
the predicate can be used as a constraint:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
?- X :: 1 .. 10, notin3to6(X) infers most.
X = X{[1, 2, 7 .. 10]}
Yes (0.00s cpu)
</PRE></BLOCKQUOTE>
In this example there are no &#8220;delayed&#8221; constraints since all valuations for
<EM>X</EM> satisfying the above conditions are solutions. Propia
detects this and therefore avoids delaying the constraint
again.<BR>
<BR>
<A NAME="@default205"></A>
<A NAME="@default206"></A>
<A NAME="@default207"></A>
In scheduling
applications it is necessary to constrain two tasks that require the
same machine not to be performed at the same time.
Specifically one must end before the other begins, or vice versa.
If one task starting at time <EM>ST1</EM> has duration <EM>D1</EM> and another
task starting at time <EM>ST2</EM> has duration <EM>D2</EM>, the above
&#8220;disjunctive&#8221; constraint is
expressed as follows:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
noclash(ST1,D1,ST2,D2) :- ST1 #&gt;= ST2+D2.
noclash(ST1,D1,ST2,D2) :- ST2 #&gt;= ST1+D1.
</PRE></BLOCKQUOTE>
Generalised Propagation on this constraint allows useful information
to be extracted even before it is decided in which order the tasks
should be run:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
?- lib(ic).
...

?- [ST1, ST2] :: 1 .. 10, noclash(ST1, 5, ST2, 7) infers most.
ST1 = ST1{[1 .. 5, 8 .. 10]}
ST2 = ST2{[1 .. 3, 6 .. 10]}
There is 1 delayed goal.
Yes (0.00s cpu)
</PRE></BLOCKQUOTE>
The values <EM>6</EM> and <EM>7</EM> are removed from the domain of <EM>ST1</EM> because
the goal <CODE>noclash(ST1,5,ST2,7)</CODE> cannot be satisfied if <EM>ST1</EM> is
either <EM>6</EM> or <EM>7</EM>. For example if <EM>ST1</EM> is <EM>6</EM>, then either 
6&gt;<I>ST</I>2+7 (to satisfy the first clause defining <CODE>noclash</CODE>)
or else <I>ST</I>2&gt;6+5 (to satisfy the second clause). There is no value for
<I>ST</I>2 <I>in</I> {1...10} that makes either inequality true, and so <EM>6</EM> is
removed from the domain of <EM>ST1</EM>. By a similar reasoning
<EM>4</EM> and <EM>5</EM> are removed from the domain of <EM>ST2</EM>.<BR>
<BR>
<A NAME="@default208"></A>
We next take a simple example from propositional logic.
In this example the result of constraint propagation is reflected not
only in the variable domains, but also in the unification of problem
variables.
We first define logical conjunction by its truth table:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
land(true,true,true).
land(true,false,false).
land(false,true,false).
land(false,false,false).
</PRE></BLOCKQUOTE>
Now we ask for an <I>X</I>,<I>Y</I>,<I>Z</I> satisfying
<I>land</I>(<I>X</I>,<I>Y</I>,<I>Z</I>) &and; <I>X</I>=<I>Y</I>.
Both solutions have <I>X</I>=<I>Y</I>=<I>Z</I>, and this information is produced solely
by propagating on the <CODE>land</CODE> constraint:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
?- land(X, Y, Z) infers most, X = Y.
Z = X
X = X
Y = X
There is 1 delayed goal.
Yes (0.00s cpu)
</PRE></BLOCKQUOTE>
<A NAME="@default209"></A>
We now illustrate the potential efficiency benefits of Generalised
Propagation with a simple resource allocation 
problem. A company makes 9 products, each of which require two kinds
of components in their manufacture, and yields a certain profit.
This information is held in the following table.
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
/*** product(Name,#Component1,#Component2,Profit). **/
product(1,1,19,1).
product(2,2,17,2).
product(3,3,15,3).
product(4,4,13,4).
product(5,10,8,5).
product(6,16,4,4).
product(7,17,3,3).
product(8,18,2,2).
product(9,19,1,1).
</PRE></BLOCKQUOTE>
We wish to find which products to manufacture in order to make a
certain profit without 
using more than a certain number of either kind of
component.<SUP><A NAME="text5" HREF="libman038.html#note5">1</A></SUP><BR>
<BR>
We first define a predicate <CODE>sum(Products,Comp1,Comp2,Profit)</CODE>
which relates a list of products (eg <CODE>Products</CODE>=<CODE>[1,5,1]</CODE>), 
to the number of each component required to build all the products in the list
and the profit
(for <CODE>[1,5,1]</CODE>, <CODE>Comp1=12</CODE> and <CODE>Comp2=46</CODE> and
<CODE>Profit=7</CODE>).
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
sum([],0,0,0).
sum([Name|Products],Count1,Count2,Profit) :- 
    [Count1,Count2,Profit]::0..100,
    product(Name,Ct1a,Ct2a,Profita),
    Count1 #= Ct1a+Ct1b,
    Count2 #= Ct2a+Ct2b,
    Profit #= Profita+Profitb,
    sum(Products,Ct1b,Ct2b,Profitb).
</PRE></BLOCKQUOTE>
If <CODE>sum</CODE> is invoked with a list of variables as its first argument,
eg <CODE>[V1,V2,V3]</CODE>, then the only choice made during execution is at
the call to <CODE>product</CODE>. In short, for each variable in the input
list there are <EM>9</EM> alternative products that could be chosen.
For a list of three variables there are consequently
9<SUP>3</SUP>= 729
alternatives.<BR>
<BR>
If we assume a production batch of <EM>9</EM> units, then the number of
alternative ways of solving <CODE>sum</CODE> is
9<SUP>9</SUP>
, or nearly 400
million. To avoid exploring so many possibilities, we simply annotate
the call to <CODE>product(Name,Ct1a,Ct2a,Profita)</CODE> as a Generalised
Propagation constraint.
Thus the new definition of <CODE>sum</CODE> is:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
sum([],0,0,0).
sum([Name|Products],Count1,Count2,Profit) :- 
    [Count1,Count2,Profit]::0..100,
    product(Name,Ct1a,Ct2a,Profita) infers most,
    Count1 #= Ct1a+Ct1b,
    Count2 #= Ct2a+Ct2b,
    Profit #= Profita+Profitb,
    sum(Products,Ct1b,Ct2b,Profitb).
</PRE></BLOCKQUOTE>
Now <CODE>sum</CODE> refuses to make any choices:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
?- sum([V1, V2, V3], Comp1, Comp2, Profit).
V1 = V1{1 .. 9}
V2 = V2{1 .. 9}
V3 = V3{1 .. 9}
Comp1 = Comp1{3 .. 57}
Comp2 = Comp2{3 .. 57}
Profit = Profit{3 .. 15}
There are 9 delayed goals.
Yes (0.01s cpu)
</PRE></BLOCKQUOTE> 
Using the second version of <CODE>sum</CODE>,
it is simple to write a program which produces lists of products
which use less than a given number <CODE>Max1</CODE> and <CODE>Max2</CODE> of each
component, and yields more than a given profit <CODE>MinProfit</CODE>: 
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim"> 
solve(Products,Batch,Max1,Max2,MinProfit) :-
    length(Products,Batch),
    Comp1 #=&lt; Max1,
    Comp2 #=&lt; Max2,
    Profit #&gt;= MinProfit,
    sum(Products,Comp1,Comp2,Profit),
    labeling(Products).
</PRE></BLOCKQUOTE>
The following query finds which products to manufacture in order to make a
profit of 40 without 
using more than 95 of either kind of component.
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
?- solve(P, 9, 95, 95, 40).
P = [1, 4, 5, 5, 5, 5, 5, 5, 5]
Yes (0.03s cpu, solution 1, maybe more)
</PRE></BLOCKQUOTE>
Constraints can be dropped as soon
as they became redundant (i.e. as soon as they were entailed by the
current partial solution).
The check for entailment can be expensive, so Propia only drops
constraints if a simple syntactic check allows it.
For <EM>infers most</EM>, this check succeeds if the <CODE>IC</CODE>
library is loaded, and the constraint has only one remaining variable.<BR>
<BR>
<HR>
<A HREF="libman039.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="libman038.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="libman041.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
</BODY>
</HTML>
